s SubGrp of g
== s(e) & (a:|g|. (s(a))  (s(~(a)))) & (a, b:|g|. (s(a))  (s(b))  (s(a * b))) 

latex

---

clarification:

s SubGrp of g
== s(eg)
== & (a:|g|. (s(a))  (s((~g)(a))))
== & (a:|g|, b:|g|. (s(a))  (s(b))  (s(a (*g) b))) 

latex

Up	groups 1
Wellformedness Lemmas	subgrp p wf
Definitions	e, P & Q, ~, x:A. B(x), |g|, P  Q, x f y, *